f(s(X)) → f(X)
g(cons(0, Y)) → g(Y)
g(cons(s(X), Y)) → s(X)
h(cons(X, Y)) → h(g(cons(X, Y)))
↳ QTRS
↳ DependencyPairsProof
f(s(X)) → f(X)
g(cons(0, Y)) → g(Y)
g(cons(s(X), Y)) → s(X)
h(cons(X, Y)) → h(g(cons(X, Y)))
H(cons(X, Y)) → H(g(cons(X, Y)))
F(s(X)) → F(X)
H(cons(X, Y)) → G(cons(X, Y))
G(cons(0, Y)) → G(Y)
f(s(X)) → f(X)
g(cons(0, Y)) → g(Y)
g(cons(s(X), Y)) → s(X)
h(cons(X, Y)) → h(g(cons(X, Y)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
H(cons(X, Y)) → H(g(cons(X, Y)))
F(s(X)) → F(X)
H(cons(X, Y)) → G(cons(X, Y))
G(cons(0, Y)) → G(Y)
f(s(X)) → f(X)
g(cons(0, Y)) → g(Y)
g(cons(s(X), Y)) → s(X)
h(cons(X, Y)) → h(g(cons(X, Y)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
G(cons(0, Y)) → G(Y)
f(s(X)) → f(X)
g(cons(0, Y)) → g(Y)
g(cons(s(X), Y)) → s(X)
h(cons(X, Y)) → h(g(cons(X, Y)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
G(cons(0, Y)) → G(Y)
The value of delta used in the strict ordering is 1/16.
POL(cons(x1, x2)) = (1/4)x_1 + (4)x_2
POL(G(x1)) = (1/4)x_1
POL(0) = 1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
f(s(X)) → f(X)
g(cons(0, Y)) → g(Y)
g(cons(s(X), Y)) → s(X)
h(cons(X, Y)) → h(g(cons(X, Y)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
F(s(X)) → F(X)
f(s(X)) → f(X)
g(cons(0, Y)) → g(Y)
g(cons(s(X), Y)) → s(X)
h(cons(X, Y)) → h(g(cons(X, Y)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(s(X)) → F(X)
The value of delta used in the strict ordering is 1/16.
POL(s(x1)) = 1/4 + (2)x_1
POL(F(x1)) = (1/4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
f(s(X)) → f(X)
g(cons(0, Y)) → g(Y)
g(cons(s(X), Y)) → s(X)
h(cons(X, Y)) → h(g(cons(X, Y)))